Church's thesis (constructive mathematics)

In constructive mathematics, Church's thesis is the mathematical assertion that all total functions are recursive. It gets its name after the informal Church–Turing thesis, which states that every algorithm is in fact a recursive function, but the constructivist version is formal and much stronger. It is in fact incompatible with classical logic.

Formal statement

One way Church's Thesis can be formally stated is by the schema:

$(\forall x \; \exist y \; \phi(x,y)) \to (\exist f \; \forall x \;\exist y,u \; \bold{T}(f,x,y,u) \wedge \phi(x,y))$

Where the variables range over the natural numbers, and $\phi$ is any predicate. This schema asserts that, if for every x there is a y satisfying some predicate, then there is in fact an f which is the Gödel number of a general recursive function which will, for every x, produce such a y satisfying that predicate. (T is some universal predicate which decodes the Gödel-numbering used.)

The thesis is incompatible with classical logic; adding it to Heyting arithmetic (HA) allows one to disprove instances of the law of the excluded middle. For instance, it is a classical tautology that every Turing machine either halts or does not halt on a given input; but if that were true, then from Church's Thesis one would conclude that there is a general recursive function which solves the halting problem. This is impossible.

However, Heyting arithmetic is equiconsistent with Peano arithmetic (PA) as well as with Heyting arithmetic plus Church's thesis. That is, adding either the law of the excluded middle or Church's thesis can not make Heyting arithmetic inconsistent, but adding both will.

Extended Church's thesis

Extended Church's thesis (ECT) extends the claim to functions which are totally defined over a certain type of domain. It is used by the school of constructive mathematics founded by Andrey Markov Jr. It can be formally stated by the schema:

$(\forall x \; \psi(x) \to \exist y \; \phi(x,y)) \to \exist f (\forall x \; \psi(x) \to \exist y,u \; \bold{T}(f,x,y,u) \wedge \phi(x,y))$

In the above, $\psi$ is restricted to be almost-negative. For first-order arithmetic (where the schema is designated $ECT_0$ ), this means $\psi$ cannot contain any disjunction, and existential quantifiers can only appear in front of $\Delta^0_0$ (decidable) formulas.

This thesis can be characterised as saying that a sentence is true if and only if it is computably realisable. In fact this is captured by the following meta-theoretic equivalences^[1]:

$HA %2B ECT_0 \vdash (\phi \leftrightarrow (\exist n \; n \Vdash \phi))$

$(HA %2B ECT_0 \vdash \phi) \leftrightarrow (HA \vdash \exist n \; (n \Vdash \phi))$

Here, $n \Vdash \phi$ stands for " $n \text{ realises } \phi$ ". So, it is provable in $HA$ with $ECT_0$ that a sentence is true iff it is realisable. But also, $\phi$ is provably true in $HA$ with $ECT_0$ iff $\phi$ is provably realisable in $HA$ without $ECT_0$ .

The second equivalence can be extended with Markov's principle (M) as follows:

$(HA %2B ECT_0 %2B M \vdash \phi) \leftrightarrow (\exist n \; PA \vdash (\bar{n} \Vdash \phi))$

So, $\phi$ is provably true in $HA$ with $ECT_0$ and $M$ iff there is a number n which provably realises $\phi$ in $PA$ . The existential quantifier has to be outside $PA$ in this case, because PA is non-constructive and lacks the existence property.

Reference

^ Troelstra, A. S. Metamathematical investigation of intuitionistic arithmetic and analysis. Vol 344 of Lecture notes in mathematics; Springer, 1973